COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	It now seems reasonable to include circumscription in EKL.  The command
C00004 ENDMK
C⊗;
It now seems reasonable to include circumscription in EKL.  The command
should have the form

(circumscribe <linerange> <predsyms> <indvars> <wff>)

The formula to be produced has the form

A(P1,...,Pn) ∧ ∀P1' ... Pn'.
	(A(P1', ... ,Pn')
	∧ (∀x1 ... xm.(E(P1i, ... Pni,x1, ... ,xn) ⊃ E(P1, ... Pn,x1, ... ,xm))
	⊃ (∀x1 ... xm.(E(P1, ... Pn,x1, ... ,xn) ≡ E(P1', ... Pn,x1, ... ,xm))

Here P1,...,Pn are the predicate symbols and x1, ... xm are the
invidividual variables.  Actually they are predicate symbols and
individual variables only relative to the formual and may be of any
types.  A(P1,...Pn) is the conjunction of the line range.  Usually,
the Ps will be some of the predicates occurring in the line range, but
no harm will be done if some extra P s are included.  A(P1',...,Pn') is
the result of replacing the Pi s by corresponding predicate variables Pi'
in the conjunction A.  E(P1,...,Pn,x1,...,xm) is the wff to be
circumscribed (minimized).  The result is a kind of assumption,
but perhaps it should be treated differently from other assumptions,
since it isn't intended to be discharged.